Nuprl Definition : msga 0,22

MsgA
== ds:x:Id fp Type
== da:a:Knd fp Type
== x:Id fp ds(x)?Void
== a:Id fp State(ds)Valtype(da;locl(a))Prop
== kx:KndId fp State(ds)Valtype(da;1of(kx))ds(2of(kx))?Void
== kl:KndIdLnk fp (tg:Id(State(ds)Valtype(da;1of(kl))(da(rcv(2of(kl),tg))?Void List))) List
== x:Id fp Knd List
== ltg:IdLnkId fp Knd List
== k:Knd fp Id List
== k:Knd fp IdLnk List
== x:Id fp Knd List
== Top 
latex



clarification:

msga{i:l}
== ds:x:Id fp Type{i}
== da:a:Knd fp Type{i}
== x:Id fp fpf-cap(ds;IdDeq;x;Void)
== a:Id fp State(ds)Valtype(da;locl(a))Prop{i}
== kx:KndId fp State(ds)Valtype(da;1of(kx))fpf-cap(ds;IdDeq;2of(kx);Void)
== kl:KndIdLnk fp
== (tg:Id(State(ds)Valtype(da;1of(kl))(fpf-cap(da;KindDeq;rcv(2of(kl),tg);Void) List))) List
== x:Id fp Knd List
== ltg:IdLnkId fp Knd List
== k:Knd fp Id List
== k:Knd fp IdLnk List
== x:Id fp Knd List
== Top 
latex


DefinitionsType, locl(a), Prop, IdDeq, State(ds), x:AB(x), Valtype(da;k), 1of(t), f(x)?z, KindDeq, rcv(l,tg), 2of(t), Void, IdLnk, x:AB(x), a:A fp B(a), Id, type List, Knd, Top
FDL editor aliasesmsga

origin